NIL 


(DEFPROP DIR
 (NIL DIR
      TAUT
      TAUT1
      SIMP
      SIMPNOT
      SIMPOR
      SIMPAND
      SIMPANDOR
      SIMPIMP
      SIMPEQUIV
      MKOR
      MKAND
      MKOR1
      MKAND1
      PN
      FIRSTVAR
      FIRSTVAR1
      FIRSTVAR2)
VALUE)

(DEFPROP TAUT
 (LAMBDA (WFF) (TAUT1 (SIMP WFF)))
EXPR)

(DEFPROP TAUT1
 (LAMBDA(W)
  (COND ((ISCONST W) W) (T (TAUT ((LAMBDA (X) (MKAND (SUBST T X W) (SUBST NIL X W))) (FIRSTVAR W))))))
EXPR)

(DEFPROP SIMPNOT
 (LAMBDA (W) (COND ((ISFALSE W) T) ((ISTRUE W) NIL) (T (MKNOT W))))
EXPR)

(DEFPROP SIMPOR
 (LAMBDA (W1 W2) (SIMPANDOR (QUOTE OR) W1 W2 W1 W2))
EXPR)

(DEFPROP SIMPAND
 (LAMBDA (W1 W2) (SIMPANDOR (QUOTE AND) W1 W2 W2 W1))
EXPR)

(DEFPROP SIMPANDOR
 (LAMBDA(OP W1 W2 V1 V2)
  (COND ((ISTRUE W1) V1) ((ISTRUE W2) V2) ((ISFALSE W1) V2) ((ISFALSE W2) V1) (T (MKOP OP W1 W2))))
EXPR)

(DEFPROP SIMPIMP
 (LAMBDA (W1 W2) (SIMPOR (SIMPNOT W1) W2))
EXPR)

(DEFPROP SIMPEQUIV
 (LAMBDA (W1 W2) (SIMPAND (SIMPIMP W1 W2) (SIMPIMP W2 W1)))
EXPR)

(DEFPROP MKOR
 (LAMBDA (V L) (MKOR1 V (REST L) (MKAND W (REVERSE (FIRST L)))))
EXPR)

(DEFPROP MKAND
 (LAMBDA(V L)
  (COND	((ZEROP (FIRST L)) NIL)
	(T (MKAND1 (REST V) (REST (REST L)) (COND ((ZEROP L) (MK_NOT (FIRST L))) (T (FIRST V)))))))
EXPR)

(DEFPROP MKOR1
 (LAMBDA(V L1 L2)
  (COND ((NULL L1) L2) (T (MKOR1 V (REST L1) (MKOP (QUOTE OR) (MKAND V (REVERSE (FIRST L1))) L2)))))
EXPR)

(DEFPROP MKAND1
 (LAMBDA(V L1 L2)
  (COND	((NULL L1) L2)
	(T (MKAND1 (REST V) (REST L1) (MKOP (QUOTE AND) (COND ((ZEROP L1) (MK_NOT (FIRST V))) (T (FIRST V)))))))
  L2)
EXPR)

(DEFPROP PN
 (LAMBDA(WFF Z)
  (COND	((ATOM WFF) (COND ((ISOR Z) (MKNOT WFF)) (T WFF)))
	((ISNOT WFF) (PN (BODY WFF) (FLIP Z)))
	(ISEQUIV WFF)
	(MKOP Z (MKOP (FLIP Z)))))
EXPR)

(DEFPROP FIRSTVAR
 (LAMBDA (W) (FIRSTVAR1 W NIL))
EXPR)

(DEFPROP FIRSTVAR1
 (LAMBDA(W VAR)
  (COND	((NOT (NULL VAR)) VAR)
	((ISCONST W) NIL)
	((ISVAR W) W)
	((UNARY W) (FIRSTVAR1 (BODY W) NIL))
	(T (FIRSTVAR1 (LHS W) ((LAMBDA (X) (COND (X X) (T (FIRSTVAR1 (RHS W) NIL)))) (RHS W))))))
EXPR)

(DEFPROP FIRSTVAR2
 (LAMBDA(W)
  (COND	((ISVAR W) W)
	((UNARY W) (FIRSTVAR (BODY W)))
	((FIRSTVAR (LHS W)) (T (FIRSTVAR (RHS W))))
	(DE SIMP
	    (W)
	    (COND ((OR (ISCONST W) (ISVAR W)) W)
		  ((ISNOT W) (SIMPNOT (SIMP W)))
		  ((ISOR W) (SIMPOR (SIMP (ARG1 W)) (SIMP (ARG2 W))))
		  ((ISAND W) (SIMPAND (SIMP (ARG1 W)) (SIMP (ARG2 W))))
		  ((ISIMP W) (SIMPIMP (SIMP (ARG1 W)) (SIMP (ARG2 W))))
		  ((ISEQUIV W) (SIMPEQUIV (SIMP (ARG1 W)) (SIMP (ARG2 W))))))))
EXPR)

NIL